Improve performance for large projects #4419

keyboardDrummer · 2023-08-15T10:08:18Z

Changes

Sample sending notifications to the IDE, so at most one is sent every 100ms. Relatedly, IdeState is computed lazily, so it is not computed for notifications that are not sent to the IDE.
Cancel ongoing compilation work and notification publishing immediately when UpdateDocument is entered
Start a new compilation slightly earlier, before computing the most recently changed ranges
Fix migration of recently changed ranges, so it properly accounts for Uri differences.
Optimize search for source files by starting from the common parent of all include globs instead of the disk root.
Make sure only one (correct) version of WriterFromOutputHelper is used in all test projects, to help in debugging non-deterministic failures
Small changes to IncrementalVerificationDiagnosticsBetweenMethods to help in debugging non-deterministic failures

Testing

Add a test QuickEditsInLargeFile with a 1000 line and method file, that instantly makes a 100 small edits to that file, and asserts that the language server can process these changes in at most three times as much time as it takes to open the file.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

### Changes 1. Rename `LegacySymbolTable`, which is part of the non-LSP Dafny server, to `SuperLegacySymbolTable` 1. Rename `SignatureAndCompletionTable` to `LegacySignatureAndCompletionTable` 1. Let `SignatureAndCompletionTable` differentiate between positions in different files, so it doesn't get confused between symbols in different files when they have similar positions or ranges. 1. Only migrate state in `SignatureAndCompletionTable` that relates to the changed file ### Testing - There could be a test added for 3 but I didn't add it. - Merging this PR into this other PR (#4419), reduces the time of the test `ManyFastEditsUsingLargeFilesAndIncludes` from 47 seconds to 8 seconds By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

… only using one class

…sTest

MikaelMayer

Overall according to my understanding it looks good. A few questions there and there.

Source/DafnyCore/Generic/Lazy.cs

Source/DafnyCore/Generic/Util.cs

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

MikaelMayer · 2023-08-21T18:17:30Z

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

+ lowest = Math.Min(lowest, division);
+
+ // Commented code left in intentionally
+ await output.WriteLineAsync("openMilliseconds: " + openMilliseconds);


shouldn't we use logging here instead of all these output.WriteLineAsync?

There's no logger available inside the test files.

MikaelMayer · 2023-08-21T18:18:08Z

Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs

+ await output.WriteLineAsync("changeMilliseconds: " + changeMilliseconds);
+ await output.WriteLineAsync("division: " + division);
+ try {
+ Assert.True(division < 10,


Can you please justify why this threshold? Also please consider introducing a constant at the top of the class

Source/DafnyPipeline.Test/Trivia.cs

Source/DafnyTestGeneration.Test/BasicTypes.cs

Source/DafnyTestGeneration.Test/Collections.cs

Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs

Source/DafnyTestGeneration.Test/Various.cs

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

jtristan

Can you confirm that the imports flagged as potentially not being used are in fact used or remove them? Should we add a test as suggested by Mikael?

jtristan · 2023-08-24T12:34:52Z

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

- var newRange = changeProcessor.MigrateRange(location.Range);
+ if (location.Uri != documentChange.TextDocument.Uri) {
+ return location;
+ }


Can we add one?

Source/DafnyPipeline.Test/FormatterBaseTest.cs

### Changes 1. Rename `LegacySymbolTable`, which is part of the non-LSP Dafny server, to `SuperLegacySymbolTable` 1. Rename `SignatureAndCompletionTable` to `LegacySignatureAndCompletionTable` 1. Let `SignatureAndCompletionTable` differentiate between positions in different files, so it doesn't get confused between symbols in different files when they have similar positions or ranges. 1. Only migrate state in `SignatureAndCompletionTable` that relates to the changed file ### Testing - There could be a test added for 3 but I didn't add it. - Merging this PR into this other PR (dafny-lang#4419), reduces the time of the test `ManyFastEditsUsingLargeFilesAndIncludes` from 47 seconds to 8 seconds By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

### Changes - Sample sending notifications to the IDE, so at most one is sent every 100ms. Relatedly, `IdeState` is computed lazily, so it not computed for notifications that are not sent to the IDE. - Cancel ongoing compilation work and notification publishing immediately when UpdateDocument is entered - Start a new compilation slightly earlier, before computing the most recently changed ranges - Fix migration of recently changed ranges, so it properly accounts for Uri differences. - Make sure only one (correct) version of `WriterFromOutputHelper` is used in all test projects, to help in debugging non-deterministic failures - Small changes to `IncrementalVerificationDiagnosticsBetweenMethods` to help in debugging non-deterministic failures ### Testing - Add a test `QuickEditsInLargeFile` with a 1000 line and method file, that instantly makes a 100 small edits to that file, and asserts that the language server can process these changes in at most three times as much time as it takes to open the file. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

### Changes 1. Rename `LegacySymbolTable`, which is part of the non-LSP Dafny server, to `SuperLegacySymbolTable` 1. Rename `SignatureAndCompletionTable` to `LegacySignatureAndCompletionTable` 1. Let `SignatureAndCompletionTable` differentiate between positions in different files, so it doesn't get confused between symbols in different files when they have similar positions or ranges. 1. Only migrate state in `SignatureAndCompletionTable` that relates to the changed file ### Testing - There could be a test added for 3 but I didn't add it. - Merging this PR into this other PR (#4419), reduces the time of the test `ManyFastEditsUsingLargeFilesAndIncludes` from 47 seconds to 8 seconds By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

### Changes - Sample sending notifications to the IDE, so at most one is sent every 100ms. Relatedly, `IdeState` is computed lazily, so it not computed for notifications that are not sent to the IDE. - Cancel ongoing compilation work and notification publishing immediately when UpdateDocument is entered - Start a new compilation slightly earlier, before computing the most recently changed ranges - Fix migration of recently changed ranges, so it properly accounts for Uri differences. - Make sure only one (correct) version of `WriterFromOutputHelper` is used in all test projects, to help in debugging non-deterministic failures - Small changes to `IncrementalVerificationDiagnosticsBetweenMethods` to help in debugging non-deterministic failures ### Testing - Add a test `QuickEditsInLargeFile` with a 1000 line and method file, that instantly makes a 100 small edits to that file, and asserts that the language server can process these changes in at most three times as much time as it takes to open the file. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).

keyboardDrummer added 3 commits August 15, 2023 02:07

Do not let DafnyFile already open IO resources

d8b9cad

Immediately cancel previous compilation when receiving a document update

8fb0305

Added tests

b21c716

keyboardDrummer mentioned this pull request Aug 15, 2023

Remove legacy symbol table to improve server responsiveness for large projects #4420

Open

keyboardDrummer added 4 commits August 17, 2023 13:35

Renames

409def1

Legacy symbol table differentiates between positions in different files

f3cf4dd

Update test

95a2c10

Merge branch 'betterLegacyMigration' into largeFilesTest

242655c

keyboardDrummer mentioned this pull request Aug 17, 2023

Multi-file support for legacy symbol table #4436

Merged

keyboardDrummer added 7 commits August 17, 2023 15:15

Rename test

cbf2416

Introduce cancellation to parsing

8c0075f

Draft stuff

5d14e53

Do not let DafnyFile already open IO resources

1c9450b

Introduce cancellation to parsing

b1b0e53

Ran formatter

c82ae9a

Parses error handling fixes

8f51171

keyboardDrummer added 13 commits August 18, 2023 16:40

Merge branch 'master' into parserCancellation

c557c58

Merge branch 'master' into parserCancellation

982a46f

Introduced throttle on IDE notifications

6fbe5ac

Performance fixes

fa30f38

Cleanup

f44be4e

Remove GetRootSourceUris cache

1740437

Cleanup

6230c66

Merge remote-tracking branch 'origin/master' into largeFilesTest

167c6bf

Make sure fix for WriterFromOutputHelper works across all packages by…

e3dd729

… only using one class

Merge remote-tracking branch 'fork/parserCancellation' into largeFile…

9e3c3c3

…sTest

Cleanup

dacfa78

Cleanup and fixes

3e03403

Merge commit '83a21338426~1' into largeFilesTest

a2a38bd

keyboardDrummer added 5 commits August 21, 2023 16:46

Fix used cancellationToken

81c90d4

Test improvement

f807e8e

Increase allowed division

304baef

Ran formatter

00b2ebe

Optimize file search

9eb13d0

MikaelMayer reviewed Aug 21, 2023

View reviewed changes

keyboardDrummer added 3 commits August 22, 2023 03:33

Fixes

4b26232

Comment out debug code

db4e4b2

Optimize imports

2a4f673

keyboardDrummer requested a review from MikaelMayer August 22, 2023 01:35

keyboardDrummer and others added 9 commits August 22, 2023 11:25

Fix root source file finding

897d4d6

Increase accepted division

2c1f9e1

Allow retries on the average scheduling time

126dce8

Comment out debug line

ffa0aa8

Merge branch 'master' into largeFilesTest

3a39625

Fix comp error

4c1391b

Merge remote-tracking branch 'origin/master' into largeFilesTest

cba5153

Merge branch 'master' into largeFilesTest

d710f5c

Update Source/DafnyCore/Generic/Util.cs

13e1595

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

jtristan requested changes Aug 24, 2023

View reviewed changes

Remove drive-by fix so it can be put in another PR

b866971

keyboardDrummer requested a review from jtristan August 24, 2023 13:18

jtristan approved these changes Aug 24, 2023

View reviewed changes

keyboardDrummer merged commit c547336 into dafny-lang:master Aug 24, 2023
18 checks passed

keyboardDrummer deleted the largeFilesTest branch August 24, 2023 14:29

BrewTestBot mentioned this pull request Sep 29, 2023

dafny 4.3.0 Homebrew/homebrew-core#146965

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improve performance for large projects #4419

Improve performance for large projects #4419

keyboardDrummer commented Aug 15, 2023 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Aug 21, 2023

keyboardDrummer Aug 22, 2023

MikaelMayer Aug 21, 2023

jtristan left a comment

jtristan Aug 24, 2023

Improve performance for large projects #4419

Improve performance for large projects #4419

Conversation

keyboardDrummer commented Aug 15, 2023 • edited Loading

Changes

Testing

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer Aug 21, 2023

Choose a reason for hiding this comment

keyboardDrummer Aug 22, 2023

Choose a reason for hiding this comment

MikaelMayer Aug 21, 2023

Choose a reason for hiding this comment

jtristan left a comment

Choose a reason for hiding this comment

jtristan Aug 24, 2023

Choose a reason for hiding this comment

keyboardDrummer commented Aug 15, 2023 •

edited

Loading